COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		AN EXAMPLE OF CASE ANALYSIS INVOLVING INEQUALITIES IN FOL
C00017 ENDMK
C⊗;
	AN EXAMPLE OF CASE ANALYSIS INVOLVING INEQUALITIES IN FOL

			     by John McCarthy


	For interactive computer proof-checking to become a practical
technique of program verification, we must reduce the number of steps
required in a proof.  Proving the correctness of the Takeuchi function
provides an entry into an area that is insufficiently explored.  The proof
we give is longer than we would like, because FOL's REWRITE technique and
TAUTOLOGY rule, while useful, do not fully realize the possibilities of
mechanization in this area.  The area is case analysis, especially case
analysis involving an ordering relation.  Many applications of
transitivity and trichotomy are used, and there should be a technique for
doing some of the work automatically.

	The Takeuchi function is defined by

	tak(x,y,z) ← 	if x ≤ y then y
			else tak(tak(x-1,y,z), tak(y-1,z,x), tak(z-1,x,y)),

and we would like to prove that it is equal to tak0(x,y,z) given by

	tak0(x,y,z) ←	if x ≤ y then y
			else if y ≤ z then z
			else x.

"Partial correctness" is shown by proving that tak0 satisfies the functional
equation for tak, and in this FOL proof we do it by defining

	tak1(x,y,z) ←	if x ≤ y then y
			else tak0(tak0(x-1,y,z), tak0(y-1,z,x), tak0(z-1,x,y)),

and proving that tak1(x,y,z) = tak0(x,y,z).

	The proof is carried out by applying the REWRITE rule to the
wff "tak1(x,y,z) = tak0(x,y,z)" in many cases of the inequality relations
involving x, y and z.  The main case analysis is into x ≤y and ¬(x ≤ y) ∧
y ≤ z and ¬(x ≤ y) ∧ ¬(y ≤ z), i.e. it follows the definition of tak0.
The first case leads to the desired result in a single REWRITE, the second
requires two subcases each leading to a REWRITE, and the third splits into
four subcases each with a rewrite.

	In addition to the inequalities arising from the case analysis,
other inequalities are needed in the SIMPSETS in order to simplify
the conditional expression for tak1(x,y,z).  These inequalities must
be deduced from the case analysis inequalities by application of transitivity,
trichotomy and some of their simple consequences.  The axioms for inequality
are redundant, but I think they can all be regarded as included in common
knowledge about inequalities - rather than being ad hoc.  Notice that the
only property of x - 1 that is used is that it is less than x.  Proving
termination would certainly require the additional property that the
amounts to the ordering being Archimedean, i.e. that if you keep subtracting
1 from x you eventually get something smaller than y.  Maybe that's all that
is required, and it seems likely that the function would still have the
desired property for something weaker than a total ordering.

	Besides the REWRITEs, the proof contains only instantiations
of the inequality axioms, uses of the tautology rule to get inequalities
occuring in the conditional expressions, and the use of "⊃ Introduction"
and tautology in collapsing the case analysis after the cases have
been proved.

	Shortening the proof could be accomplished with the following
kinds of improvements to FOL.  (1) A goal oriented proof method that
does the case analysis, (2) An extension of the REWRITE rules that allows
using the inequality rules in REWRITE commands, the extension being
required, because they take the form of implications rather than equivalences.
(3) A special rule embodying the elementary theory of total ordering or
even Tarski's elementary theory of real numbers or some subset thereof.
All of these would be nice, although a subset might be sufficient to
make this proof small.
	
	Here are the axioms which also constitute the file TAK2.AX[F78,JMC]
at SU-AI.  If I were doing it a again, I would omit the definition of tak1
and simply reduce its right hand side.

declare INDVAR x y z ε REAL;
declare OPCONST pred(REAL) = REAL[PRE];
declare OPCONST tak0(REAL,REAL,REAL) = REAL;
declare OPCONST tak1(REAL,REAL,REAL) = REAL;
declare PREDCONST <(REAL,REAL)[L←455,R←455];
declare PREDCONST ≤(REAL,REAL)[L←455,R←455];

AXIOM LESS:
	∀x.(pred(x) < x)
	∀x.(pred(x) ≤ x)
	∀x y.((x < y ∧ ¬x=y ∧ ¬(y<x)) ∨ (¬(x<y)∧x=y∧¬(y<x)) ∨ (¬(x<y)∧¬x=y∧y<x))
	∀x y z.((x<y ∧ y<z ⊃ x<z) ∧ (x≤y ∧ y<z ⊃ x<z) ∧ (x<y ∧ y≤z ⊃ x<z)
∧ (x≤y ∧ y≤z ⊃ x≤z))
	∀x y.(x≤y ≡ x<y ∨ x=y)
	∀x.¬(x < x)
	∀x.x≤x
	∀x y.(¬(x≤y) ≡ y < x)
	∀x y.(y < x ≡ ¬(x≤y))
;;

AXIOM TAK0:
	∀x y z.(tak0(x,y,z) = IF x≤y THEN y ELSE (IF y≤z THEN z ELSE x));;
AXIOM TAK1:
	∀x y z.(tak1(x,y,z) = IF x≤y THEN y ELSE tak0(tak0(pred x,y,z),
tak0(pred y,z,x),tak0(pred z,x,y)));;

	The proof itself is 50 steps, and the three main cases end at
step 3, step 17 and step 36.  The remaining steps collapse the case
analysis, and wouldn't be required in a goal-oriented proof.

	A fuller explanation of the Takeuchi function and an informal
proof of its correctness is given in my memo "An interesting LISP function".
Further light on proof-checking via case analysis of inequalities might
be obtained by formalizing the rest of the proof.

	The proof is actually a cleaned up version of a 68 step proof that
was in some ways more informative.  Namely, I used the REWRITE rule with
what inequalities I had and looked at the right hand side to see which
ones's I still should look for.  In particular, the splitting of the main
case into subcases was determined empirically by seeing what propositional
terms appeared in the conditional expressions.  From this point of view,
FOL helped in generating the proof and didn't merely check a pre-existing
proof.


*****ASSUME x≤y;

1 x≤y  (1)

*****REWRITE tak1(x,y,z)=tak0(x,y,z) BY LOGICTREE∪{ TAK0,TAK1,1};

2 tak1(x,y,z)=tak0(x,y,z)  (1)

*****⊃I ↑↑⊃↑;

3 x≤y⊃tak1(x,y,z)=tak0(x,y,z)  

*****ASSUME ¬(x≤y);

4 ¬(x≤y)  (4)

*****REWRITE y<x BY LOGICTREE∪{ LESS9,4};

5 y<x  (4)

*****ASSUME y≤z;

6 y≤z  (6)

*****ASSUME pred x≤y;

7 pred x≤y  (7)

*****∀E LESS2 y;

8 pred y≤y  

*****∀E LESS4 pred y,y,z;

9 ((pred y<y∧y<z)⊃pred y<z)∧(((pred y≤y∧y<z)⊃pred y<z)∧(((pred y<y∧y≤z)⊃pred y<z)∧((pred y≤y∧y≤z)⊃pred y≤z)))  

*****TAUT pred y≤z 6,8:9;

10 pred y≤z  (6)

*****REWRITE tak1(x,y,z)=tak0(x,y,z) BY LOGICTREE∪{ TAK0,TAK1,4:7,10};

11 tak1(x,y,z)=tak0(x,y,z)  (4 6 7)

*****⊃I 7⊃↑;

12 pred x≤y⊃tak1(x,y,z)=tak0(x,y,z)  (4 6)

*****ASSUME ¬(pred x≤y);

13 ¬(pred x≤y)  (13)

*****REWRITE tak1(x,y,z)=tak0(x,y,z) BY LOGICTREE∪{ TAK0,TAK1,LESS7,4:6,10,13};

14 tak1(x,y,z)=tak0(x,y,z)  (4 6 13)

*****⊃I ↑↑⊃↑;

15 ¬(pred x≤y)⊃tak1(x,y,z)=tak0(x,y,z)  (4 6)

*****TAUT tak1(x,y,z)=tak0(x,y,z) 12,15;

16 tak1(x,y,z)=tak0(x,y,z)  (4 6)

*****⊃I 6⊃↑;

17 y≤z⊃tak1(x,y,z)=tak0(x,y,z)  (4)

*****ASSUME ¬(y≤z);

18 ¬(y≤z)  (18)

*****REWRITE z<y BY LOGICTREE∪{ LESS9,18};

19 z<y  (18)

*****∀E LESS4 z,y,x;

20 ((z<y∧y<x)⊃z<x)∧(((z≤y∧y<x)⊃z<x)∧(((z<y∧y≤x)⊃z<x)∧((z≤y∧y≤x)⊃z≤x)))  

*****∀E LESS5 z,x;

21 z≤x≡(z<x∨z=x)  

*****TAUT z≤x 5,19:21;

22 z≤x  (4 18)

*****∀E LESS4 pred z,z,x;

23 ((pred z<z∧z<x)⊃pred z<x)∧(((pred z≤z∧z<x)⊃pred z<x)∧(((pred z<z∧z≤x)⊃pred z<x)∧((pred z≤z∧z≤x)⊃pred z≤x)))  

*****∀E LESS2 z;

24 pred z≤z  

*****∀E LESS4 pred z,z,x;

25 ((pred z<z∧z<x)⊃pred z<x)∧(((pred z≤z∧z<x)⊃pred z<x)∧(((pred z<z∧z≤x)⊃pred z<x)∧((pred z≤z∧z≤x)⊃pred z≤x)))  

*****TAUT pred z≤x 22,24:25;

26 pred z≤x  (4 18)

*****ASSUME pred x≤y;

27 pred x≤y  (27)

*****ASSUME pred y≤z;

28 pred y≤z  (28)

*****ASSUME ¬(pred x≤y);

29 ¬(pred x≤y)  (29)

*****ASSUME ¬(pred y≤z);

30 ¬(pred y≤z)  (30)

*****REWRITE tak1(x,y,z)=tak0(x,y,z) BY FOO∪{ 27:28};

31 tak1(x,y,z)=tak0(x,y,z)  (4 18 27 28)

*****REWRITE tak1(x,y,z)=tak0(x,y,z) BY FOO∪{ 27,30};

32 tak1(x,y,z)=tak0(x,y,z)  (4 18 27 30)

*****∀E LESS4 pred x,z,y;

33 ((pred x<z∧z<y)⊃pred x<y)∧(((pred x≤z∧z<y)⊃pred x<y)∧(((pred x<z∧z≤y)⊃pred x<y)∧((pred x≤z∧z≤y)⊃pred x≤y)))  

*****∀E LESS5 z,y;

34 z≤y≡(z<y∨z=y)  

*****TAUT ¬(pred x≤z) 19,29,33:34;

35 ¬(pred x≤z)  (18 29)

*****REWRITE tak1(x,y,z)=tak0(x,y,z) BY FOO∪{ 28:29,35};

36 tak1(x,y,z)=tak0(x,y,z)  (4 18 28 29)

*****REWRITE tak1(x,y,z)=tak0(x,y,z) BY FOO∪{ 29:30};

37 tak1(x,y,z)=tak0(x,y,z)  (4 18 29 30)

*****⊃I 28⊃31;

38 pred y≤z⊃tak1(x,y,z)=tak0(x,y,z)  (4 18 27)

*****⊃I 30⊃32;

39 ¬(pred y≤z)⊃tak1(x,y,z)=tak0(x,y,z)  (4 18 27)

*****TAUT tak1(x,y,z)=tak0(x,y,z) 38:39;

40 tak1(x,y,z)=tak0(x,y,z)  (4 18 27)

*****⊃I 28⊃36;

41 pred y≤z⊃tak1(x,y,z)=tak0(x,y,z)  (4 18 29)

*****⊃I 30⊃37;

42 ¬(pred y≤z)⊃tak1(x,y,z)=tak0(x,y,z)  (4 18 29)

*****TAUT tak1(x,y,z)=tak0(x,y,z) 41:42;

43 tak1(x,y,z)=tak0(x,y,z)  (4 18 29)

*****⊃I 27⊃40;

44 pred x≤y⊃tak1(x,y,z)=tak0(x,y,z)  (4 18)

*****⊃I 29⊃↑↑;

45 ¬(pred x≤y)⊃tak1(x,y,z)=tak0(x,y,z)  (4 18)

*****TAUT tak1(x,y,z)=tak0(x,y,z) 44:45;

46 tak1(x,y,z)=tak0(x,y,z)  (4 18)

*****⊃I 18⊃↑;

47 ¬(y≤z)⊃tak1(x,y,z)=tak0(x,y,z)  (4)

*****TAUT tak1(x,y,z)=tak0(x,y,z) 17,47;

48 tak1(x,y,z)=tak0(x,y,z)  (4)

*****⊃I 4⊃↑;

49 ¬(x≤y)⊃tak1(x,y,z)=tak0(x,y,z)  

*****TAUT tak1(x,y,z)=tak0(x,y,z) 3,49;

50 tak1(x,y,z)=tak0(x,y,z)